Peano playground
Peano axioms
0 is N
a=b
a=b & b=c -> a=c
a=b & b is N -> a is N
a is N -> S(a) is N
S(a)=S(b) -> a=b
S(a)!=0
0 is K & (a is K -> S(a) is K) -> a is K
Note: '&' has more priority than '->'
Note: 'S' is a function -> What's a function?
What's 'a definition'?
What's 'a variable'?
defs
1 := S(0)
2 := S(S(0))
3: = S(S(S(0)))
TODO: +
TODO: *
TODO: divides
TODO: is prime
Theorems
1+1 = 2
2 is prime
3 is prime
Euclid's lemma
Fundamental theorem of arithmetics